Nuprl Lemma : R-and-left
11,40
postcript
pdf
A
,
B
:es_realizer{i:l},
P
:(ES{i}
{i'}).
R-Feasible{i:l}(
A
)
B
||-{i}
es
.
P
(
es
)
R-compat{i:l}(
A
;
B
)
A
B
||-{i}
es
.
P
(
es
)
latex
Definitions
P
&
Q
,
True
,
x
.
t
(
x
)
,
t
T
,
x
(
s
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
Lemmas
Rplus
wf
,
R-implies-rule
,
R-true-rule
,
es
realizer
wf
,
R-Feasible
wf
,
event
system
wf
,
R-realizes
wf
,
R-compat
wf
,
true
wf
,
R-and-rule
origin